Struct isotope::prelude::Enum [−][src]
pub struct Enum { /* fields omitted */ }
Expand description
A type with a finite number of named variants
Implementations
Compute this type’s code
Compute this type’s flags
Trait Implementations
Cons this term within a given context. Return None
if already consed.
Convert this term to it’s own consed type
Whether this term depends on a variable with a given index: if equiv is true, also consider larger variables in the same equivalence class
Get whether a term depends on a variable base <= variable <= ix
Read more
Get the variable filter of this term
type Substituted = Enum
type Substituted = Enum
The type this substitutes to
Substitute this value recursively
Convert this object’s consed form to it’s substituted form
Shift this term’s variables with index >= base
in a given context
Shift this term’s variables with index >= base
in a given context
Locally typecheck a term: note this is context-independent, without caching
Globally typecheck a term, i.e. typecheck all subterms, without caching
Typecheck this term’s annotation, without caching
Load this term’s current flags
Set this term’s flags. May cause errors if done incorrectly!
Locally typecheck a term: note this is context-independent.
Globally typecheck a term, i.e. typecheck all subterms and their variables
Variable typecheck a term, i.e. typecheck all subterms and their variables.
Typecheck this term’s annotation
Globally typecheck a term and it’s annotation, i.e. typecheck all subterms, annotation subterms, and their variables
Typecheck a term in a given context
Typecheck this term along with it’s variables
Whether this term might be type-checked
type ValueConsed = Enum
type ValueConsed = Enum
The type of value this is consed to
type ValueSubstituted = Enum
type ValueSubstituted = Enum
The type of value this is substituted to
Convert this term to a Term
, without any consing
Get the type annotation of this term
Get whether this term is a type
Get whether this term is a universe
Get whether this term is a function
Get whether this term is a dependent function type
fn annotate_unchecked(
&self,
annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Self::ValueConsed>, Error>
[src]
fn annotate_unchecked(
&self,
annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Self::ValueConsed>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in a given context
Get the hash-code of this term if it was untyped Read more
Compare this term to another within a given context
Get the index of this term in a program graph. Return None
if this term is unindexed
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in general
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]Cast this type into another in a given typing context
Substitute this term’s variables recursively given a context
Substitute this term’s variables given a context
Shift this term’s variables with index >= base
up by n
in a given context
Shift this term’s variables with index >= base
up by n
in a given context
Compare this term to a term ID, within a given context
Cons this term within a given context. Return None
if already consed.
Convert this term to a TermId
within a given context
Get the type of this term, if any
Get the type of this term, if any
Apply this value, as a function, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Apply this value, as a dependent function type, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Convert this term to a TermId
, without any consing
Clone this term to a TermId
, without any consing
Clone this term to a TermId
within a given context
Clone this term to a Term
without any consing
Shallow cons a term directly into a context
Shallow cons a term directly into a context, cloning if necessary
Convert this term to a normal form
Convert this term a normal form
Convert this term to a normal form, or reduce it up to n
steps
Convert this term a normal form, or reduce it up to n
steps
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to a normal form, or reduce it up to n
steps
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]Convert this term a normal form, or reduce it up to n
steps
Auto Trait Implementations
impl !RefUnwindSafe for Enum
impl !UnwindSafe for Enum
Blanket Implementations
Mutably borrows from an owned value. Read more
Borrow an optional value of type T
Cons this term within a given context. Return None
if already consed.
Get the type annotation of this term
Get the index of this term in an isotope
program graph, if any
Get whether this term is a type
Get whether this term is a universe
Get whether this term is in “root form”
Get whether this term is a subtype of another term in a given context
Get whether this term has a universe in all contexts
Get the untyped hash-code of this term
Get the variable filter of this term
Shift this term’s variables with index >= base
up by n
in a given context
Whether this term has a given variable dependency
Whether this term has a given variable dependency below ix
and above base
Load this term’s flags
Set this term’s flags
Compare this term to another dynamic term
Compare this term to another
Compare this term to a term ID
Compare self to key
and return true
if they are equal.